Dynamic logics (DL) are mutli-modal logics, where modalities are parameterised over actions from some action language. The action language may be a programming language, or consist of system (or component) level steps, or of environment moves. In this talk, I introduce principles of DL, and show how DL based verification can be practically used to verify programs. In particular, I will show how the KeY system supports dynamic logic based verification of some mainstream programming languages.

Slides: [Part 1], [Part 2], [Part 3], [Part 4], [Part 5]

The correctness of real-time systems, that mix concurrency with hard timing constraints, is important, yet challenging to achieve. Formal verification techniques such as model checking provide guarantees of correctness. This course will focus on timed automata, an extension of finite-state automata with clocks measuring the elapsing of time, and on (timed) temporal logics; it will provide an overview of the concepts in this area. The course will also mention parametric timed formalisms, turning very useful when the system is not known with full precision, or at early design stages. Depending on the time, practical sessions may be organized.

Slides: [Part 1], [Part 2], [Part 3]

Motivated by the remarkable advances in machine learning (ML), there exists a pressing need to build trust in the operation of ML models, especially for those that target high-risk uses. One main goal of explainable artificial intelligence (XAI) is to deliver trustworthy AI, by enabling human decision makers to fathom the operation of ML models. Unfortunately, the most visible XAI solutions are riddled with misconceptions, and so computed explanations offer no guarantees of rigor. Formal (or symbolic) XAI represents a solution to the pitfalls of informal XAI that has been under active development in recent years. This lecture offers an overview of the emerging field of symbolic XAI, covering its main achievements, but also the challenges that it still faces.

[Slides]

Formal methods offer rigorous assurances of correctness for both hardware and software systems. Their use is well established in industry, notably to certify safety of critical applications subjected to stringent certification processes. With the rising prominence of machine learning, the integration of machine-learned components into critical systems presents novel challenges for the soundness, precision, and scalability of formal methods.

This lecture serves as an introduction to formal methods tailored for machine learning pipelines, highlighting their strengths and limitations. We will present several approaches through the lens of different software properties and targeting software across all phases of a machine learning pipeline, with a focus on abstract interpretation-based techniques. We will then conclude by offering perspectives for future research directions in this evolving context.

[Slides]

The formal verification of hard- and software, with techniques such as model checking and deductive verification, is computationally very demanding. Graphics Processing Units (GPUs) have been increasingly successful in pushing the boundaries of the state-of-the-art in many research fields, with their application to AI being the latest prominent success. This course will address how GPUs can be used to accelerate formal verification.

The focus will first be on the basics of GPU programming. You will get hands-on experience with the Single Instruction Multiple Threads execution model, and iteratively optimise an initial CUDA program to use the various features of NVIDIA’s GPUs. Next, you will apply this knowledge to accelerate computations relevant for formal verification, including graph analysis and SAT solving. How these computations fit in the bigger picture of formal verification tools will be discussed, including a comparison of relevant algorithms.

Slides: [Part1], [Part2]